T:Type, l1, l2:T List. l1 || l2  (l:T List. l1  l & l2  l) 

latex

Definitions	P  Q, P  Q, P  Q, l1 || l2, x:A. B(x), P & Q, Prop, l1  l2, x:A. B(x), t  T, P  Q
Lemmas	common iseg compat, iseg weakening, iseg wf, compat wf